Problem:
 rev(a()) -> a()
 rev(b()) -> b()
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(++(x,x)) -> rev(x)

Proof:
 Complexity Transformation Processor:
  strict:
   rev(a()) -> a()
   rev(b()) -> b()
   rev(++(x,y)) -> ++(rev(y),rev(x))
   rev(++(x,x)) -> rev(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [++](x0, x1) = x0 + x1 + 69,
     
     [b] = 0,
     
     [rev](x0) = x0,
     
     [a] = 33
    orientation:
     rev(a()) = 33 >= 33 = a()
     
     rev(b()) = 0 >= 0 = b()
     
     rev(++(x,y)) = x + y + 69 >= x + y + 69 = ++(rev(y),rev(x))
     
     rev(++(x,x)) = 2x + 69 >= x = rev(x)
    problem:
     strict:
      rev(a()) -> a()
      rev(b()) -> b()
      rev(++(x,y)) -> ++(rev(y),rev(x))
     weak:
      rev(++(x,x)) -> rev(x)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [++](x0, x1) = x0 + x1,
       
       [b] = 1,
       
       [rev](x0) = x0 + 4,
       
       [a] = 8
      orientation:
       rev(a()) = 12 >= 8 = a()
       
       rev(b()) = 5 >= 1 = b()
       
       rev(++(x,y)) = x + y + 4 >= x + y + 8 = ++(rev(y),rev(x))
       
       rev(++(x,x)) = 2x + 4 >= x + 4 = rev(x)
      problem:
       strict:
        rev(++(x,y)) -> ++(rev(y),rev(x))
       weak:
        rev(a()) -> a()
        rev(b()) -> b()
        rev(++(x,x)) -> rev(x)
      Matrix Interpretation Processor:
       dimension: 5
       max_matrix:
        [1 1 1 0 1]
        [0 0 0 0 0]
        [0 0 0 0 0]
        [0 0 0 0 0]
        [0 0 0 0 1]
        interpretation:
                        [1 0 0 0 0]     [1 1 1 0 0]     [0]
                        [0 0 0 0 0]     [0 0 0 0 0]     [0]
         [++](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0]
                        [0 0 0 0 0]     [0 0 0 0 0]     [0]
                        [0 0 0 0 1]     [0 0 0 0 1]     [1],
         
               [0]
               [0]
         [b] = [0]
               [0]
               [0],
         
                     [1 0 0 0 1]  
                     [0 0 0 0 0]  
         [rev](x0) = [0 0 0 0 0]x0
                     [0 0 0 0 0]  
                     [0 0 0 0 1]  ,
         
               [0]
               [0]
         [a] = [0]
               [0]
               [0]
        orientation:
                        [1 0 0 0 1]    [1 1 1 0 1]    [1]    [1 0 0 0 1]    [1 0 0 0 1]    [0]                    
                        [0 0 0 0 0]    [0 0 0 0 0]    [0]    [0 0 0 0 0]    [0 0 0 0 0]    [0]                    
         rev(++(x,y)) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0] = ++(rev(y),rev(x))
                        [0 0 0 0 0]    [0 0 0 0 0]    [0]    [0 0 0 0 0]    [0 0 0 0 0]    [0]                    
                        [0 0 0 0 1]    [0 0 0 0 1]    [1]    [0 0 0 0 1]    [0 0 0 0 1]    [1]                    
         
                    [0]    [0]      
                    [0]    [0]      
         rev(a()) = [0] >= [0] = a()
                    [0]    [0]      
                    [0]    [0]      
         
                    [0]    [0]      
                    [0]    [0]      
         rev(b()) = [0] >= [0] = b()
                    [0]    [0]      
                    [0]    [0]      
         
                        [2 1 1 0 2]    [1]    [1 0 0 0 1]          
                        [0 0 0 0 0]    [0]    [0 0 0 0 0]          
         rev(++(x,x)) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x = rev(x)
                        [0 0 0 0 0]    [0]    [0 0 0 0 0]          
                        [0 0 0 0 2]    [1]    [0 0 0 0 1]          
        problem:
         strict:
          
         weak:
          rev(++(x,y)) -> ++(rev(y),rev(x))
          rev(a()) -> a()
          rev(b()) -> b()
          rev(++(x,x)) -> rev(x)
        Qed